T:Type, l1,l2:(T List). iseg(T; l1; l2)  (||l1||  ||l2||) 

latex

Definitions	prop{i:l}, t  T, x:A. B(x), iseg(T; l1; l2), P  Q, x:A. B(x), P  Q, True, T, P  Q, P  Q
Lemmas	append wf, length wf1, le wf, non neg length, length append, true wf, squash wf